
module Hw1_grader(Hw1 : Hw1) : Grader.Sig =
struct 

let _ = unset_jrh_lexer 

open OUnit

let t1 = `:bool`
let t2 = `:nat`
let t3 = `:real`
let t4 = `:int`
let t5 = `:nat#nat`
let t6 = `:nat->real`
let t7 = `:real->bool`
let t8 = `:nat->bool`
let t9 = `:(nat->bool)->bool`
let t10 = `:(real->bool)->bool`

let p1 = `T`
let p2 = `F`
let p3 = `P ==> Q`
let p4 = `P <=> Q`
let p5 = `~P`
let p6 = `~P ==> Q`
let p7 = `F ==> P`
let p8 = `P ==> F`
let p9 = `(T ==> P) <=> P`
let p10 = `(P ==> Q) <=> (~Q ==> ~P)`
let p11 = `!x. x * x >= &0`
let p12 = `!y. ?m. y < m`
let p13 = `?x. X x`
let p14 = `?X. !x. ~(X x)`
let p15 = `f x > g y`
let p16 = `x = y ==> f x = g y`
let p17 = `&0 < &1 / &2 /\ &1 / &2 < &1`
let p18 = `!x y. ~(x = y) ==> ~(f x = f y)`
let p19 = `!x. ?y. f y = x`
let p20 = `!e. e > &0 ==> ?d. abs(x - y) < e ==> abs (f x - f y) < d`
let p21 = `A SUBSET B`
let p22 = `A INTER B = C`
let p23 = `A UNION B = C`
let p24 = `A INTER B = B INTER A`
let p25 = `A UNION B SUBSET C`
let p26 = `?n. &2 pow n > &17`
let p27 = `?n. &2 pow n > &777 / &1000`
let p28 = `(&3:int) - &4 = -- &1`
let p29 = `&3 - &4 = -- &1`
let p30 = `--(-- &4) + &3 - &7`
let p31 = `&3 + (-- &4)`
let p32 = `&1 / &0`
let p33 = `UNIONS X = C`
let p34 = `{}`
let p35 = `{}`
let p36 = `(1, 2)`
let p37 = `{1, 2, 3}`
let p38 = `CARD {1, 2, 3} = 3`

let h1 = `X:A`
let h2 = `x:real`
let h3 = `X:real->bool`
let h4 = `X = (UNIV:real->bool)`
let h5 = `v:real^3`
let h6 = `(v:real^3) + w`
let h7 = `X : (real->bool)->bool`
let h8 = `-- (v:real^3)`
let h9 = `(v:real^3) $ 3`
let h10 = `&3 % (v:real^3)`
let h11 = `(v:real^3) dot w`
let h12 = `&2 % (v:real^3) + &4 % w - &7 % u`

let mk_type_test (n, p, q) = n >:: (fun () -> if p = q then () else raise (Failure ""))

let can_match p q = 
  try
    ignore(term_match [] p q)
    ; true
  with _ -> false 

let can_matchl ps q = List.exists (fun p -> can_match p q) ps

let mk_term_test (n, p, q) = n >:: (fun () -> if can_match p q then () else raise (Failure ""))

(* let mk_term_test (n, ps, q) = n >:: (fun () -> if can_matchl ps q then () else raise Fail "")  *)

(* let _ = set_jrh_lexer *)
(* let mk_term_test (n, p, q) = *)
(*   let rewrites = [SUBSET; IN] in *)
(*     n >:: (fun () -> ignore(MESON rewrites (mk_eq(p, q)))) *)
(* let _ = unset_jrh_lexer *)

let types =
  "Types" >:::
    (map mk_type_test
       [ ("t1", t1, Hw1.t1)
       ; ("t2", t2, Hw1.t2)
       ; ("t3", t3, Hw1.t3)
       ; ("t4", t4, Hw1.t4)
       ; ("t5", t5, Hw1.t5)
       ; ("t6", t6, Hw1.t6)
       ; ("t7", t7, Hw1.t7)
       ; ("t8", t8, Hw1.t8)
       ; ("t9", t9, Hw1.t9)
       ; ("t10", t10, Hw1.t10)
       ])

let terms = 
  "Terms" >:::
    (map mk_term_test
       [ ("p1", p1, Hw1.p1)
       ; ("p2", p2, Hw1.p2)
       ; ("p3", p3, Hw1.p3)
       ; ("p4", p4, Hw1.p4)
       ; ("p5", p5, Hw1.p5)
       ; ("p6", p6, Hw1.p6)
       ; ("p7", p7, Hw1.p7)
       ; ("p8", p8, Hw1.p8)
       ; ("p9", p9, Hw1.p9)
       ; ("p10", p10, Hw1.p10)
       ; ("p11", p11, Hw1.p11)
       ; ("p12", p12, Hw1.p12)
       ; ("p13", p13, Hw1.p13)
       ; ("p14", p14, Hw1.p14)
       ; ("p15", p15, Hw1.p15)
       ; ("p16", p16, Hw1.p16)
       ; ("p17", p17, Hw1.p17)
       ; ("p18", p18, Hw1.p18)
       ; ("p19", p19, Hw1.p19)
       ; ("p20", p20, Hw1.p20)
       ; ("p21", p21, Hw1.p21)
       ; ("p22", p22, Hw1.p22)
       ; ("p23", p23, Hw1.p23)
       ; ("p24", p24, Hw1.p24)
       ; ("p25", p25, Hw1.p25)
       ; ("p26", p26, Hw1.p26)
       ; ("p27", p27, Hw1.p27)
       ; ("p28", p28, Hw1.p28)
       ; ("p29", p29, Hw1.p29)
       ; ("p30", p30, Hw1.p30)
       ; ("p31", p31, Hw1.p31)
       ; ("p32", p32, Hw1.p32)
       ; ("p33", p33, Hw1.p33)
       ; ("p34", p34, Hw1.p34)
       ; ("p35", p35, Hw1.p35)
       ; ("p36", p36, Hw1.p36)
       ; ("p37", p37, Hw1.p37)
       ; ("p38", p38, Hw1.p38)
       ])

let ascribe =
  "Ascriptions" >:::
    (map mk_term_test
       [ ("h1", h1, Hw1.h1)
       ; ("h2", h2, Hw1.h2)
       ; ("h3", h3, Hw1.h3)
       ; ("h4", h4, Hw1.h4)
       ; ("h5", h5, Hw1.h5)
       ; ("h6", h6, Hw1.h6)
       ; ("h7", h7, Hw1.h7)
       ; ("h8", h8, Hw1.h8)
       ; ("h9", h9, Hw1.h9)
       ; ("h10", h10, Hw1.h10)
       ; ("h11", h11, Hw1.h11)
       ; ("h12", h12, Hw1.h12)
       ])

let test = "HW1" >::: [types; terms; ascribe]

let _ = set_jrh_lexer 

end
